Step of Proof: minus_imin 12,41
Inference at * 1 0 
Iof proof for Lemma minus imin:



1. a : 
2. b : 
  (-if a z b then a else b fi ) = if (-a) z -b then -b else -a fi  
latex
 by PERMUTE{1:n,
 by PERMUTE{2:n,
 by PERMUTE{3:n,
 by PERMUTE{4:n,
 by PERMUTE{5:n,
 by PERMUTE{6:n,
 by PERMUTE{7:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{12:n,
 by PERMUTE{13:n,
 by PERMUTE{14:n,
 by PERMUTE{15:n,
 by PERMUTE{16:n,
 by PERMUTE{17:n,
 by PERMUTE{18:n,
 by PERMUTE{19:n,
 by PERMUTE{20:n,
 by PERMUTE{18:n,
 by PERMUTE{21:n,
 by PERMUTE{19:n,
 by PERMUTE{22:n,
 by PERMUTE{23:n,
 by PERMUTE{24:n,
 by PERMUTE{25:n,
 by PERMUTE{26:n,
 by PERMUTE{24:n,
 by PERMUTE{23:n,
 by PERMUTE{27:n,
 by PERMUTE{28:n,
 by PERMUTE{29:n,
 by PERMUTE{30:n,
 by PERMUTE{28:n,
 by PERMUTE{31:n,
 by PERMUTE{29:n,
 by PERMUTE{32:n,
 by PERMUTE{33:n,
 by PERMUTE{34:n,
 by PERMUTE{35:n,
 by PERMUTE{36:n,
 by PERMUTE{34:n,
 by PERMUTE{33:n,
 by PERMUTE{37:n,
 by PERMUTE{38:n,
 by PERMUTE{39:n,
 by PERMUTE{40:n,
 by PERMUTE{41:n,
 by PERMUTE{42:n,
 by PERMUTE{43:n,
 by PERMUTE{44:n,
 by PERMUTE{45:n,
 by PERMUTE{46:n,
 by PERMUTE{47:n,
 by PERMUTE{48:n,
 by PERMUTE{46:n,
 by PERMUTE{49:n,
 by PERMUTE{47:n,
 by PERMUTE{50:n,
 by PERMUTE{51:n,
 by PERMUTE{52:n,
 by PERMUTE{53:n,
 by PERMUTE{54:n,
 by PERMUTE{52:n,
 by PERMUTE{51:n,
 by PERMUTE{55:n} 
latex

 1: .....wf..... NILNIL

 1:   a z b  
 2: .....wf..... NILNIL

 2:     Type
 3: .....wf..... NILNIL

 3: 3. a z b = tt
 3:   (a z b = tt)  
 4: .....wf..... NILNIL

 4: 3. a z b = tt
 4:   (a z b)  
 5: .....wf..... NILNIL

 5: 3. a z b = tt
 5:   (a  b)  
 6: .....wf..... NILNIL

 6: 3. a z b = tt
 6:   a z b  
 7: .....wf..... NILNIL

 7: 3. a z b = tt
 7:   a  
 8: .....wf..... NILNIL

 8: 3. a z b = tt
 8:   b  
 9: .....wf..... NILNIL

 9: 3. a  b
 9:   (-a) z -b  
 10: .....wf..... NILNIL

 10: 3. a  b
 10:     Type
 11: .....wf..... NILNIL

 11: 3. a  b
 11: 4. (-a) z -b = tt
 11:   ((-a) z -b = tt)  
 12: .....wf..... NILNIL

 12: 3. a  b
 12: 4. (-a) z -b = tt
 12:   ((-a) z -b)  
 13: .....wf..... NILNIL

 13: 3. a  b
 13: 4. (-a) z -b = tt
 13:   ((-a)  (-b))  
 14: .....wf..... NILNIL

 14: 3. a  b
 14: 4. (-a) z -b = tt
 14:   (-a) z -b  
 15: .....wf..... NILNIL

 15: 3. a  b
 15: 4. (-a) z -b = tt
 15:   (-a)  
 16: .....wf..... NILNIL

 16: 3. a  b
 16: 4. (-a) z -b = tt
 16:   (-b)  
 17: .....truecase..... NILNIL

 17: 3. a  b
 17: 4. (-a)  (-b)
 17:   (-a) = (-b)
 18: .....wf..... NILNIL

 18: 3. a  b
 18: 4. (-a) z -b = ff
 18:   ((-a) z -b = ff)  
 19: .....wf..... NILNIL

 19: 3. a  b
 19: 4. (-a) z -b = ff
 19:   ((-b) <z (-a))  
 20: .....wf..... NILNIL

 20: 3. a  b
 20: 4. (-a) z -b = ff
 20:   ((-b) < (-a))  
 21: .....wf..... NILNIL

 21: 3. a  b
 21: 4. (-a) z -b = ff
 21:   (((-a) z -b))  
 22: .....wf..... NILNIL

 22: 3. a  b
 22: 4. (-a) z -b = ff
 22:   (-a) z -b  
 23: .....wf..... NILNIL

 23: 3. a  b
 23: 4. (-a) z -b = ff
 23:   (-a)  
 24: .....wf..... NILNIL

 24: 3. a  b
 24: 4. (-a) z -b = ff
 24:   (-b)  
 25: .....antecedent..... NILNIL

 25: 3. a  b
 25: 4. (-a) z -b = ff
 25:   True
 26: .....wf..... NILNIL

 26: 3. a  b
 26: 4. (-a) z -b = ff
 26: 5. (((-a) z -b)) = ((-b) <z (-a))
 26:    = 
 27: .....falsecase..... NILNIL

 27: 3. a  b
 27: 4. (-b) < (-a)
 27:   (-a) = (-a)
 28: .....wf..... NILNIL

 28: 3. a z b = ff
 28:   (a z b = ff)  
 29: .....wf..... NILNIL

 29: 3. a z b = ff
 29:   (b <z a)  
 30: .....wf..... NILNIL

 30: 3. a z b = ff
 30:   (b < a)  
 31: .....wf..... NILNIL

 31: 3. a z b = ff
 31:   ((a z b))  
 32: .....wf..... NILNIL

 32: 3. a z b = ff
 32:   a z b  
 33: .....wf..... NILNIL

 33: 3. a z b = ff
 33:   a  
 34: .....wf..... NILNIL

 34: 3. a z b = ff
 34:   b  
 35: .....antecedent..... NILNIL

 35: 3. a z b = ff
 35:   True
 36: .....wf..... NILNIL

 36: 3. a z b = ff
 36: 4. ((a z b)) = (b <z a)
 36:    = 
 37: .....wf..... NILNIL

 37: 3. b < a
 37:   (-a) z -b  
 38: .....wf..... NILNIL

 38: 3. b < a
 38:     Type
 39: .....wf..... NILNIL

 39: 3. b < a
 39: 4. (-a) z -b = tt
 39:   ((-a) z -b = tt)  
 40: .....wf..... NILNIL

 40: 3. b < a
 40: 4. (-a) z -b = tt
 40:   ((-a) z -b)  
 41: .....wf..... NILNIL

 41: 3. b < a
 41: 4. (-a) z -b = tt
 41:   ((-a)  (-b))  
 42: .....wf..... NILNIL

 42: 3. b < a
 42: 4. (-a) z -b = tt
 42:   (-a) z -b  
 43: .....wf..... NILNIL

 43: 3. b < a
 43: 4. (-a) z -b = tt
 43:   (-a)  
 44: .....wf..... NILNIL

 44: 3. b < a
 44: 4. (-a) z -b = tt
 44:   (-b)  
 45: .....truecase..... NILNIL

 45: 3. b < a
 45: 4. (-a)  (-b)
 45:   (-b) = (-b)
 46: .....wf..... NILNIL

 46: 3. b < a
 46: 4. (-a) z -b = ff
 46:   ((-a) z -b = ff)  
 47: .....wf..... NILNIL

 47: 3. b < a
 47: 4. (-a) z -b = ff
 47:   ((-b) <z (-a))  
 48: .....wf..... NILNIL

 48: 3. b < a
 48: 4. (-a) z -b = ff
 48:   ((-b) < (-a))  
 49: .....wf..... NILNIL

 49: 3. b < a
 49: 4. (-a) z -b = ff
 49:   (((-a) z -b))  
 50: .....wf..... NILNIL

 50: 3. b < a
 50: 4. (-a) z -b = ff
 50:   (-a) z -b  
 51: .....wf..... NILNIL

 51: 3. b < a
 51: 4. (-a) z -b = ff
 51:   (-a)  
 52: .....wf..... NILNIL

 52: 3. b < a
 52: 4. (-a) z -b = ff
 52:   (-b)  
 53: .....antecedent..... NILNIL

 53: 3. b < a
 53: 4. (-a) z -b = ff
 53:   True
 54: .....wf..... NILNIL

 54: 3. b < a
 54: 4. (-a) z -b = ff
 54: 5. (((-a) z -b)) = ((-b) <z (-a))
 54:    = 
 55: .....falsecase..... NILNIL

 55: 3. b < a
 55: 4. (-b) < (-a)
 55:   (-b) = (-a)
 .

Definitions{x:A| B(x)} , x.A(x), b, i <z j, a < b, inr x , case b of inl(x) => s(x) | inr(y) => t(y), x:A  B(x), b, f(a), A  B, , Ax, #$n, inl x , left + right, x:AB(x), Type, i z j, -n, s = t, , , Unit, , True, T, ff, P  Q, P & Q, P  Q, tt, P  Q, x:A. B(x), t  T, if b then t else f fi 
Lemmasbool wf, true wf, squash wf, assert of lt int, bnot of le int, assert wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity

origin